<html>
<head><meta charset="utf-8"><title>Featherweight Rust · wg-formal-methods · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/index.html">wg-formal-methods</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Featherweight.20Rust.html">Featherweight Rust</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="194432229"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Featherweight%20Rust/near/194432229" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicolas Osborne <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Featherweight.20Rust.html#194432229">(Apr 17 2020 at 12:32)</a>:</h4>
<p>Hello everyone,<br>
I am not sure it is the right place to ask this, but: is the analog of Featherweight Java had been define for Rust ?</p>



<a name="194433566"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Featherweight%20Rust/near/194433566" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> bjorn3 <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Featherweight.20Rust.html#194433566">(Apr 17 2020 at 12:43)</a>:</h4>
<p><a href="https://plv.mpi-sws.org/rustbelt/" title="https://plv.mpi-sws.org/rustbelt/">https://plv.mpi-sws.org/rustbelt/</a></p>



<a name="194435364"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Featherweight%20Rust/near/194435364" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicolas Osborne <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Featherweight.20Rust.html#194435364">(Apr 17 2020 at 12:58)</a>:</h4>
<p>Yes, this is a fascinating project. But if I remember correctly, they define Lambda-Rust which is a separation logic and is expressed in continuation passing style. I was thinking of a language close to Rust but with less features.</p>



<a name="194435780"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Featherweight%20Rust/near/194435780" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> simulacrum <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Featherweight.20Rust.html#194435780">(Apr 17 2020 at 13:01)</a>:</h4>
<p>You may be interested in e.g. sealed rust</p>



<a name="194436113"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Featherweight%20Rust/near/194436113" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> bjorn3 <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Featherweight.20Rust.html#194436113">(Apr 17 2020 at 13:03)</a>:</h4>
<p>As far as I know sealed rust is still a concept.</p>



<a name="194436160"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Featherweight%20Rust/near/194436160" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> simulacrum <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Featherweight.20Rust.html#194436160">(Apr 17 2020 at 13:03)</a>:</h4>
<p>yes, though there's active work on it</p>



<a name="194436242"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Featherweight%20Rust/near/194436242" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicolas Osborne <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Featherweight.20Rust.html#194436242">(Apr 17 2020 at 13:04)</a>:</h4>
<p>This is exactly what I was thinking about ! Thanks.</p>



<a name="194550082"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Featherweight%20Rust/near/194550082" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Vytautas Astrauskas [he/him] <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Featherweight.20Rust.html#194550082">(Apr 18 2020 at 15:29)</a>:</h4>
<p><a href="https://arxiv.org/pdf/1903.00982.pdf" title="https://arxiv.org/pdf/1903.00982.pdf">https://arxiv.org/pdf/1903.00982.pdf</a></p>



<a name="194550268"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Featherweight%20Rust/near/194550268" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Shnatsel <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Featherweight.20Rust.html#194550268">(Apr 18 2020 at 15:33)</a>:</h4>
<p>one of the authors, Niko Matsakis, is in this chat - you can talk to them if you wish.</p>



<a name="194550956"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Featherweight%20Rust/near/194550956" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicolas Osborne <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Featherweight.20Rust.html#194550956">(Apr 18 2020 at 15:47)</a>:</h4>
<p>That's even better. Many thanks.</p>



<a name="194584591"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Featherweight%20Rust/near/194584591" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Featherweight.20Rust.html#194584591">(Apr 19 2020 at 07:46)</a>:</h4>
<p>Note though that that paper contains some flaws (it's a preprint, not a reviewed published paper). the authors are working on a significantly improved next version. not sure if that is already available somewhere.</p>



<a name="194584607"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Featherweight%20Rust/near/194584607" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Featherweight.20Rust.html#194584607">(Apr 19 2020 at 07:47)</a>:</h4>
<p><span class="user-mention" data-user-id="127262">@Aaron Weiss</span>, another author of that paper, is also here in this chat and might know ;)</p>



<a name="194584612"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Featherweight%20Rust/near/194584612" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Featherweight.20Rust.html#194584612">(Apr 19 2020 at 07:48)</a>:</h4>
<p>and btw I'm one of the authors of the rustbelt paper mentioned above</p>



<a name="194591078"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Featherweight%20Rust/near/194591078" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicolas Osborne <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Featherweight.20Rust.html#194591078">(Apr 19 2020 at 10:44)</a>:</h4>
<p>I really enjoyed the rustbelt paper (I didn't understand all of it, I have to work a bit more :-) )</p>
<p>In the context of the compilation course for my master degree, I am implementing something like a borrow-checker. But, on the side, I am interested in investigating whether it is possible to implement a compilator "correct by construction" for a very little language (like Imp in <em>Software Foundations</em>) in Agda. (Here, correct means with semantic preservation).</p>
<p>For now, I am just experimenting in expressing syntax and semantics.  The first step would be to have a type-checker correct by construction like what did McBride and McKinna for the simply typed lambda calculus in <em>The view from the left</em>. So, I am drawn in puting more features in the language like functions and affine type system.</p>



<a name="194592828"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Featherweight%20Rust/near/194592828" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Featherweight.20Rust.html#194592828">(Apr 19 2020 at 11:26)</a>:</h4>
<p>that sounds like a fun project :D</p>



<a name="194689160"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Featherweight%20Rust/near/194689160" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Aaron Weiss <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Featherweight.20Rust.html#194689160">(Apr 20 2020 at 15:15)</a>:</h4>
<p><span class="user-mention silent" data-user-id="120791">RalfJ</span> <a href="#narrow/stream/183875-wg-formal-methods/topic/Featherweight.20Rust/near/194584607" title="#narrow/stream/183875-wg-formal-methods/topic/Featherweight.20Rust/near/194584607">said</a>:</p>
<blockquote>
<p><span class="user-mention silent" data-user-id="127262">Aaron Weiss</span>, another author of that paper, is also here in this chat and might know ;)</p>
</blockquote>
<p>I am indeed here, and happy to answer any questions. There has indeed been a lot of fixes to Oxide since that draft was uploaded, but I will hopefully be uploading a new (and hopefully much-improved) draft in the next few weeks.</p>



<a name="201034858"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Featherweight%20Rust/near/201034858" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Andrea Lattuada <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Featherweight.20Rust.html#201034858">(Jun 16 2020 at 15:47)</a>:</h4>
<p>Hi <span class="user-mention" data-user-id="127262">@Aaron Weiss</span>. Is the updated draft available somewhere? I’m in a reasearch group that’s very interested in the intersection between the borrow checker and software verification (we’re aware and very keen of Prusti).</p>



<a name="201266090"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Featherweight%20Rust/near/201266090" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Andrea Lattuada <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Featherweight.20Rust.html#201266090">(Jun 18 2020 at 13:19)</a>:</h4>
<p><span class="user-mention silent" data-user-id="116852">Andrea Lattuada</span> <a href="#narrow/stream/183875-wg-formal-methods/topic/Featherweight.20Rust/near/201034858">said</a>:</p>
<blockquote>
<p>Hi <span class="user-mention silent" data-user-id="127262">Aaron Weiss</span>. Is the updated draft available somewhere? I’m in a reasearch group that’s very interested in the intersection between the borrow checker and software verification (we’re aware and very keen of Prusti).</p>
</blockquote>
<p>cc <span class="user-mention" data-user-id="116009">@nikomatsakis</span> Is an updated draft of the Oxide paper available somewhere?</p>



<a name="205803173"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Featherweight%20Rust/near/205803173" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nathan Lilienthal <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Featherweight.20Rust.html#205803173">(Aug 03 2020 at 14:52)</a>:</h4>
<p><span class="user-mention" data-user-id="266274">@Nicolas Osborne</span>:</p>
<blockquote>
<p>But, on the side, I am interested in investigating whether it is possible to implement a compilator "correct by construction" for a very little language (like Imp in <em>Software Foundations</em>) in Agda. (Here, correct means with semantic preservation).</p>
</blockquote>
<p>I read <a href="https://people.csail.mit.edu/jgross/personal-website/papers/2015-jgross-thesis.pdf">this thesis</a> a while back, which you may find interesting, regardless of what it is you actually build. It draws some parallels between proof trees and parse trees in Coq, yielding verified parsers as a result.</p>
<blockquote>
<p>For now, I am just experimenting in expressing syntax and semantics.  The first step would be to have a type-checker correct by construction like what did McBride and McKinna for the simply typed lambda calculus in <em>The view from the left</em>. So, I am drawn in puting more features in the language like functions and affine type system.</p>
</blockquote>
<p>Neat, I haven't seen that paper! How are you parsing and evaluating the syntax? I've used <a href="https://github.com/lalrpop/lalrpop">LALRPOP</a> in the past for very simple things and been really happy, and I've seen starts to the full Rust language in it.</p>



<a name="205807249"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Featherweight%20Rust/near/205807249" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Featherweight.20Rust.html#205807249">(Aug 03 2020 at 15:21)</a>:</h4>
<p>did you mean to reply to this topic? i can't see the messages you were quoting but they seem interesting</p>



<a name="205808068"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Featherweight%20Rust/near/205808068" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nathan Lilienthal <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Featherweight.20Rust.html#205808068">(Aug 03 2020 at 15:28)</a>:</h4>
<p><span class="user-mention" data-user-id="312719">@Xavier Denis</span> I did mean to reply here, though I'll admit to being a new Zulip user who may be doing it wrong. IDK why the messages aren't visible, perhaps I loaded them a while back without realizing.</p>



<a name="205841939"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Featherweight%20Rust/near/205841939" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lqd <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Featherweight.20Rust.html#205841939">(Aug 03 2020 at 20:13)</a>:</h4>
<p>btw we have an update to the previous question: Aaron mentioned earlier that they would upload the latest Oxide draft very soon (depending on internet connectivity)</p>



<a name="206875812"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Featherweight%20Rust/near/206875812" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Aaron Weiss <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Featherweight.20Rust.html#206875812">(Aug 13 2020 at 21:47)</a>:</h4>
<p>Sorry, I haven’t been active on Zulip! Didn’t have it installed on anything, but the latest draft is now on my website and should hit arXiv soon (and includes the full appendix this time): <a href="https://aaronweiss.us/pubs/draft20-oxide.pdf">https://aaronweiss.us/pubs/draft20-oxide.pdf</a></p>



<a name="206875863"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Featherweight%20Rust/near/206875863" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Aaron Weiss <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Featherweight.20Rust.html#206875863">(Aug 13 2020 at 21:47)</a>:</h4>
<p>Feel free to ping me here (I’ll actually see it now) or email me if you have any questions, comments, etc.</p>



<a name="206875956"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Featherweight%20Rust/near/206875956" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Aaron Weiss <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Featherweight.20Rust.html#206875956">(Aug 13 2020 at 21:48)</a>:</h4>
<p>The delay from when I had said “next few weeks” was the result of stumbling onto a bunch more work to be done, unfortunately.</p>



<a name="206911657"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Featherweight%20Rust/near/206911657" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> lqd <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Featherweight.20Rust.html#206911657">(Aug 14 2020 at 09:24)</a>:</h4>
<p>(just in case people haven't seen it there's also a repo for the implementation and test suite at <a href="https://github.com/aatxe/oxide">https://github.com/aatxe/oxide</a>)</p>



<a name="207510796"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Featherweight%20Rust/near/207510796" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nicolas Osborne <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Featherweight.20Rust.html#207510796">(Aug 20 2020 at 11:06)</a>:</h4>
<p><span class="user-mention" data-user-id="245809">@Nathan Lilienthal</span> <br>
Sorry for the late answer.<br>
Thanks for the pointers. Actually, I don't really bother with parsing for now. I just work on abstract syntax, but this is good to know.</p>



<a name="223485582"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Featherweight%20Rust/near/223485582" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Bas Spitters <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Featherweight.20Rust.html#223485582">(Jan 21 2021 at 09:32)</a>:</h4>
<p><span class="user-mention" data-user-id="127262">@Aaron Weiss</span> Thanks for the interesting work on Oxide. What is the status of your Coq formalization?</p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>